(set-logic QF_ABV)
(set-option :bv-solver bitblast-internal)
(set-option :incremental true)
(declare-const v (_ BitVec 1))
(declare-fun a () (Array (_ BitVec 8) (_ BitVec 8)))
(assert (and (= (store a (_ bv0 8) (_ bv0 8)) (store a (_ bv0 8) (bvadd (_ bv1 8) ((_ zero_extend 7) v))))))
(set-info :status unsat)
(check-sat)
(set-info :status unsat)
(check-sat)
